r:CRng, a:|r|, n:. ((1 +r (-r(a))) * ((r) 0  i < n. a r i)) = (1 +r (-r(a r n)))  |r| 

latex

Definitions

False, A, A  B, P  Q, t  T, x:A. B(x), P & Q, x. t(x), P  Q, P  Q, x f y, , , Rng, CRng, i  j < k, x(s), {i..j},

Lemmas

le wf, crng wf, rng car wf, nat wf, rng plus zero, rng plus inv, rng minus zero, rng times zero, rng times over minus, rng zero wf, rng times over plus, rng nexp zero, int seg wf, rng nexp wf, rng sum unroll base, rng minus wf, rng one wf, rng plus wf, rng times wf, rng sum wf, rng sum unroll hi, rng plus inv assoc, rng plus comm, rng plus ac 1, rng plus assoc, crng times comm, rng times one, rng nexp unroll